automode to choose from a dropdown list#3857
Conversation
|
Drafting for now, since it was unstable so far and can have one more round of UI testing. |
|
As soon as the proof scripts are on the main branch, another button for the script-aware autopilot should be added. |
|
Can we maybe workshop a better name for the regular automation? "Full Automation" vs. "Full Auto Pilot" is not exactly user friendly. Perhaps "Apply Strategy"? |
|
Great idea! Concerning:
Maybe sth along the lines Full Automation (Efficient) <-- former Apply Strategy One could then have small tooltip explaining
|
|
I like your UI-concerns. Thanks for rasing them. To unify the concepts: "Apply strategy" should be part of the macro context menu. How about the following?
|
mattulbrich
force-pushed
the
automodeDropdown
branch
from
20d101b to
a494361
Compare
|
I have updated the UX according to our plan. |
| * @see de.uka.ilkd.key.macros.FullAutoPilotProofMacro | ||
| */ | ||
| public static Icon automationFullPilotLogo(int size) { | ||
| return automationWithOverlay(size, "F"); |
There was a problem hiding this comment.
I hate to be nit-picky but "S" makes more sense for the structural auto pilot, imo
| return automationWithOverlay(size, "F"); | |
| return automationWithOverlay(size, "S"); |
3 participants
Related Issue
n/a
Intended Change
Currently, only the full automation is on a button in the toolbar. But the autopilots have reached a similar degree of relevance and will even more with the JML proof scripts.
Plan
Type of pull request
New feature (non-breaking change which adds functionality)
A small UI feature that we had discussed already a few times.
Ensuring quality
Manually
Additional information and contact(s)
Co-Authored by: kit.qwen3.5-397b-A17b @ KIT, Local AI
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.